The present disclosure relates generally to testing of circuit designs, and more particularly to guided exploration of circuit design states.
Circuit designs with digital logic can be represented as finite state machines. A finite state machine for a circuit design can be visualized as a directed graph that comprises nodes and edges connecting the nodes. The nodes represent states of the circuit design, and the edges represent transitions between the states of the circuit design. Exploring the state-space of a circuit design has a number of useful purposes, such as verifying properties of the circuit design, justifying the reachability of a given state for an equivalence checker, generating tests to satisfy missing coverage, analyzing RTL code to understand behavior, etc.
One technique for exploring the state-space of a circuit design is known as bounded model checking (BMC). BMC techniques attempts to exhaustively check all possible behaviors of the circuit design by starting at particular state and exploring all states that are reachable from that state within a fixed number of steps. However, one of the most serious challenges with model checking techniques is the state-space explosion problem. As the size and complexity of a circuit design grows, so do the number of states that need to be explored. The state-space for a circuit design can be very large, making it impossible to explore the entire state-space with limited resources of time and memory. As a result, conventional BMC techniques are useful for hitting shallow target states, but are unable to explore deep into the state-space for large circuit designs.